#topos theory

[pv1isalsoimportant]

(Semi-regularly updated) list of resources for (not only) young mathematicians interested in logic and all things related:

Igor Oliveira's survey article on the main results from complexity theory and bounded arithmetic is a good starting point if you're interested in these topics

Eitetsu Ken's list for resources on proof complexity, computational complexity, logic, graph theory, finite model theory, combinatorial game theory and type theory

The Complexity Zoo for information on complexity classes

The Proof Complexity Zoo for information on proof systems and relationships between them

Computational Complexity blog for opinions and interesting blog posts about computational complexity and bunch of other stuff

Student logic seminar's home page for worksheets on proof complexity and bounded arithmetic (great introduction for beginners)

Jan Krajíček's personal page is full of old teaching materials and resources for students (click past teaching). I also recommend checking out his books. They are basically the equivalent of a bible for this stuff, although they are a bit difficult to read.

Amir Akbar Tabatabai's page for materials on topos theory and categories including lecture notes and recording of lectures

Lean Game Server for learning the proof assistant Lean by playing fun games

[m---a---x]

Welcome to the premier of One-Picture-Proof!

This is either going to be the first installment of a long running series or something I will never do again. (We'll see, don't know yet.)

Like the name suggests each iteration will showcase a theorem with its proof, all in one picture. I will provide preliminaries and definitions, as well as some execises so you can test your understanding. (Answers will be provided below the break.)

The goal is to ease people with some basic knowledge in mathematics into set theory, and its categorical approach specifically. While many of the theorems in this series will apply to topos theory in general, our main interest will be the topos Set. I will assume you are aware of the notations of commutative diagrams and some terminology. You will find each post to be very information dense, don't feel discouraged if you need some time on each diagram. When you have internalized everything mentioned in this post you have completed weeks worth of study from a variety of undergrad and grad courses. Try to work through the proof arrow by arrow, try out specific examples and it will become clear in retrospect.

Please feel free to submit your solutions and ask questions, I will try to clear up missunderstandings and it will help me designing further illustrations. (Of course you can just cheat, but where's the fun in that. Noone's here to judge you!)

Preliminaries and Definitions:

B^A is the exponential object, which contains all morphisms A→B. I comes equipped with the morphism eval. : A×(B^A)→B which can be thought of as evaluating an input-morphism pair (a,f)↦f(a).

The natural isomorphism curry sends a morphism X×A→B to the morphism X→B^A that partially evaluates it. (1×A≃A)

φ is just some morphism A→B^A.

Δ is the diagonal, which maps a↦(a,a).

1 is the terminal object, you can think of it as a single-point set.

We will start out with some introductory theorem, which many of you may already be familiar with. Here it is again, so you don't have to scroll all the way up:

Exercises:

What is the statement of the theorem?

Work through the proof, follow the arrows in the diagram, understand how it is composed.

What is the more popular name for this technique?

What are some applications of it? Work through those corollaries in the diagram.

Can the theorem be modified for epimorphisms? Why or why not?

For the advanced: What is the precise requirement on the category, such that we can perform this proof?

For the advanced: Can you alter the proof to lessen this requirement?

Bonus question: Can you see the Sicko face? Can you unsee it now?

Expand to see the solutions:

Solutions:

This is Lawvere's Fixed-Point Theorem. It states that, if there is a point-surjective morphism φ:A→B^A, then every endomorphism on B has a fixed point.

Good job! Nothing else to say here.

This is most commonly known as diagonalization, though many corollaries carry their own name. Usually it is stated in its contraposition: Given a fixed-point-less endomorphism on B there is no surjective morphism A→B^A.

Most famous is certainly Cantor's Diagonalization, which introduced the technique and founded the field of set theory. For this we work in the category of sets where morphisms are functions. Let A=ℕ and B=2={0,1}. Now the function 2→2, 0↦1, 1↦0 witnesses that there can not be a surjection ℕ→2^ℕ, and thus there is more than one infinite cardinal. Similarly it is also the prototypiacal proof of incompletness arguments, such as Gödels Incompleteness Theorem when applied to a Gödel-numbering, the Halting Problem when we enumerate all programs (more generally Rice's Theorem), Russells Paradox, the Liar Paradox and Tarski's Non-Defineability of Truth when we enumerate definable formulas or Curry's Paradox which shows lambda calculus is incompatible with the implication symbol (minimal logic) as well as many many more. As in the proof for Curry's Paradox it can be used to construct a fixed-point combinator. It also is the basis for forcing but this will be discussed in detail at a later date.

If we were to replace point-surjective with epimorphism the theorem would no longer hold for general categories. (Of course in Set the epimorphisms are exactly the surjective functions.) The standard counterexample is somewhat technical and uses an epimorphism ℕ→S^ℕ in the category of compactly generated Hausdorff spaces. This either made it very obvious to you or not at all. Either way, don't linger on this for too long. (Maybe in future installments we will talk about Polish spaces, then you may want to look at this again.) If you really want to you can read more in the nLab page mentioned below.

This proof requires our category to be cartesian closed. This means that it has all finite products and gives us some "meta knowledge", called closed monoidal structure, to work with exponentials.

Yanofsky's theorem is a slight generalization. It combines our proof steps where we use the closed monoidal structure such that we only use finite products by pre-evaluating everything. But this in turn requires us to introduce a corresponding technicallity to the statement of the theorem which makes working with it much more cumbersome. So it is worth keeping in the back of your mind that it exists, but usually you want to be working with Lawvere's version.

Yes you can. No, you will never be able to look at this diagram the same way again.

We see that Lawvere's Theorem forms the foundation of foundational mathematics and logic, appears everywhere and is (imo) its most important theorem. Hence why I thought it a good pick to kick of this series.

If you want to read more, the nLab page expands on some of the only tangentially mentioned topics, but in my opinion this suprisingly beginner friendly paper by Yanofsky is the best way to read about the topic.

[ms-foobles]

IF 𝒞 IS A TOPOS THEN 𝒞↓I IS ALSO A TOPOS FOR ALL OBJECTS I??????!!?!!!!!

[max1461]

california bans riemannian geometry because it is kinda white supremacist to put a metric on a manifold. florida bans topos theory becuase grothendieck was Woke

[proof-by-intimidation]

alright, Lurie's higher topos theory hits so hard. Can't wait to get into it seriously

[geronimosothercadilac]

Art Theory - The reason why people think Geronimo Stilton is not male.

First look how masculine Geronimo Stilton is in earlier illustrations like this one below.

Think again:-

He looks noticeably slimmer and more like a fox/jackal. Notice how feminine he looks in this remake of this one above.

The Theory - Possible attempt to make character appeal to female audiences. Another thing is that he is based on a combination of famous literary personalities like most detectives (Sherlock Holmes, Hercule Poirot and more), other rats (like those of Beatrix Potter or Anthony Browne), and Lewis Carroll's Alice! His features (physical and mental) might be taken from those characters. Interestingly enough, those are all British works I mentioned, however he may also be influenced by Topo Gigio (Italian cartoon series).

[branded-perceptions]

Motivating vs justifying reasons:

without motivation no observation which simultaneously is an ACTION

that in the realm of quantum scale is bound to via subjective decision of observation SIMULTANEOUSLY ACT UPON / alter objective reality in order to measure it which we then justify / explain subjectively via our reductionistic (like a computer compressing) consciousness made up of fictional numeric and linguistic SYMBOLS🎅 that we collectively our subjective emotions attach to

our social desires (and the resulting actions that alter reality according to) what we subjectively long for and thus collectively compete to create (and "race" for / chase mimetically wanting "more" ... "mehr") like past colonialism is defined by HOW / what we "observe" and make sense of ... the socio-psychological metaphor "Quantum observer effect" at "SCALE" (double-entendre: dimension vs "SEEsaw"⚖️) which requires proactive metacognitive BALANCE to make sure in by our habits

(what we "SEE" depends on the filtering of our mind symbols whose order and connotations depend on what we "SAW" in the past)

defined motivational competitions' psychotically self-justifying in-group identity "races" (competitive group chases for via shared symbols convergerted goals, behaviours and identities) collective attention shadows happens no injust causal abuse like "racism".

a behaviour or moral in-group justification that to one group ("kin") appears as "kind" or "go(o)d"🤥😷😇 might appear to another "party" or group ("kin") as "hatred" or "bad": these PSYCHOLOGICAL "quantum fluctuations" in "deCOHERENCE" (📚Free energy principle by Karl Friston) of in-groups' symbolic (sinn bolic) understandings can now be better conveyed and discussed via help of music pattern bridging logos, mythos and underlying emotions, metaphorically flirting with each other's sense-makings instead of physically fighting:

our subjective sense-makings are constructed via and defined by our collective sense-makings and emotionally stabilised via grouped🏟👏👏👏 symbolic🎅 constructs' argumentative team identitifications. No one of us has ever had an "independent" or "individual" mind, but tend to arrogantly believe otherwise. But some introspect more than others and thus learn to evaluate and especially in moral contexts (Immanuel Kant) create social differentiations and symbolic groupings more autonomously with an intrinsic compass.

Everything we think or communicate is inevitably a lie to a certain degree as we are bound to need to compress data of objective systems reality in order to fit into reductionistic psychological symbolic🎅 representations of it like linguistics or algebra that thus has inevitable blind spots as explored by Higher topos theory Jacob Lurie which we can only strive to handle responsibly via proactive curiosity about subjective UNfamiliarity of everything that might not be represented by familiARITY (in-group identifications "ARITY master functions" as used in AI-TECH) of our symbolic subjective perceptions and interpretations of objective reality.

Irony is the mimetic tool to communicate and dialectically evolve that: both linguistically and mathematically (ponder about the meaning of mathematic 0).

the emotional charging of dominance of linguistic / numeric symbolic🎅 constructs' explanatory reductionism of an in-group define what "MATTERS" to / is perceived as "real" (matter) and worthy of pursued by them, emotionally calibrating their motivations and out of this resulting curvature of psychotic justifications we tend to confuse with reason: 🔍list of psychological (group) biases.

https://twitter.com/BEFREEtoSEE/status/1788485006567850320

[fundgruber]

Dietmar Dath - Neptunation.

Die Oktopoden werden uns verbinden, wenn wir es nach oben schaffen

Die Mission ist die Verbindung

Connection, Funktoren zwischen Kategorien von Kategorien, zwischen höheren Topoi

Bei Dietmar Dath ist Mathematik zur sozialen Bewegung, zum Implex geworden, eine Diktatur der Programmierer*innen und der Wissenschaft, in der Topos-Coding der Skill ist mit dem Aufhebung funktioniert, mit dem der Formwechsel der Materie gesteuert wird und die gesellschaftliche Reproduktion. In der Gegenwart codiert er selber seine Science Fiction so, mit dem Aufhebungsfunktor. Da wird dann ein Weltraumsozialismus mit transhumanistischem Gesicht (Neukörper) entworfen, in dem eine neue Politik entsteht, neue Kriege, teilweise als Wiederholungen historischer Tragödien. Die Programmierer*innen und die Wissenschaftler*innen spielen darin so eine große Rolle, weil sie im direkten Kontakt sind mit dem Management und der Spekulation. Sie haben Zugriff auf hochwertige Produktionsmittel und Gelder. Und dann im passenden Moment weichen sie ab aus den Kreisläufen des Kapitals, wie in "Menschen wie Gras", wenn die Gentechnik verfrüht freigelassen wird. Daths Faszination für China würde demnach auch nicht bedeuten das was dort passiert zu idealisieren, sondern es ist einfach ein Staat in dem diese Entwicklungen ein Stück brisanter ablaufen, wo eine KP versucht das Ganze zu steuern.

Die Grundlagen für die Freiheit zum Implex hatte eine Partei im Untergrund gelegt, sie hießen die "Gruppe Pfadintegral" (Gippies), dann die "Internationale" (eigentlich die 'Partei', aber er entschied sich dann doch für die Internationale), in unserer Welt sind das Grillabende von Wissenschaftler*innen und Radikalen, wie Barbara Kirchner irgendwo sagt, oder auch Dath immer wieder anklingen lässt. Dath ist das Aushängeschild dieser imaginären Partei (manchmal sieht man sein Formel-Tattoo auf dem Unterarm) im Hier und Jetzt, in den Büchern ist es Cordula Späth oder andere Heldinnen aus Wissenschaft und Musik. Durch seine Doppelrolle beliebter Feuilletonist bei der FAZ und Genosse der DKP zu sein streut er seinen High-Tech Marxismus in beiden Bereichen, und in Zeitschriften wie der Konkret (gerade zum Beispiel ein Text über eine Museumsausstellung über den Faschismus des 21. Jahrhunderts, genannt der "Wechselbalg", in einer zukünftigen Gesellschaft) oder bei Linken.

Die Topos-Codierung kommt auch aus der Musik, kommt auch aus der bildenden Kunst, nur haben die Gesellschaften, die Dath beschreibt das in ihre Raumgestaltung, ihre Körpergestaltung, die Gestaltung ihrer Beziehungen gelegt. Genauso wie das Gärtnern (in den Rechnergärten) oder das Kochen (deswegen auch die Bedeutung der von Dath beworbenen Bücher der Mathematikerin und Musikerin Eugenia Cheng "How to Bake Pi", und "x + y. A Mathematician’s Manifesto for Rethinking Gender", die in diesem Sinne so viel mehr sind als Einführungen). Darin liegt die verführerische Methodik der Kategorientheorie und der Topologie, Erkenntnis und Transformation auf unterschiedlichen Ebenen durchführen zu können. Und das dann wiederum mit Aufhebung zu verkabeln, mit den Klassikern:

"In early 1985, while I was studying the foundations of homotopy theory, it occurred to me that the explicit use of a certain simple categorical structure might serve as a link between mathematics and philosophy. The dialectical philosophy, developed 150 years ago by Hegel, Schleiermacher, Grassmann, Marx, and others, may provide significant insights to guide the learning and development of mathematics, while categorical precision may dispel some of the mystery in that philosophy." F. William Lawvere, Unity and Identity of Opposites in Calculus and Physics. Applied Categorical Structures 4: 167-174, 1996

Hegelianisch-Marxistische abstrakte Algebra befindet sich dann mutmaßlich im Wettstreit mit anderen diagrammatischen Methoden, wie der Lattice Theorie (vgl. Rudolf Wille, “Restructuring lattice theory: An approach based on hierarchies of concepts” 1982). Wenn seit Emmy Noether die Kartierungen Teil der mathematischen Forschung sind (vgl. Lee, C. (2013) Emmy Noether, Maria Goeppert Mayer, and their Cyborgian Counter-parts: Triangulating Mathematical-Theoretical Physics, Feminist Science Studies, and Feminist Science Fiction), bis hin zu Maryam Mirzakhani (in der Nachruferzählung und in der Raumerzählung "Du bist mir gleich" wird das was diese Mathematik mit dem Denken macht in seiner Tragik und transformativen Kraft spürbar), dann ist das was die Netzwerk-Coder (z.B. Fan/Gao/Luo (2007) "Hierarchical classication for automatic image annotation", Eler/Nakazaki/Paulovich/Santos/Andery/Oliveira/Neto/Minghim (2009) "Visual analysis of image collections") und Google Arts & Culture in die digitale Kunstwissenschaft eingeführt haben, man kann es nicht anders sagen, das Gegenteil von all dem. Unhinterfragte Kategorien und unhinterfragte konzeptuelle Graphen (also sowohl Lattice Theorie, als auch Topologie ignorierend), werden ohne Binaritäten oder Äquivalente einfach als gerichtete Graphen, entweder strukturiert von den alten Ordnungen, oder, das soll dann das neue sein, als Mapping von visueller Ähnlichkeit gezeigt (vgl. die Umap Projekte von Google oder das was die Staatlichen Museen als Visualisierungs-Baustein in der neuen Version ihrer online Sammlung veröffentlicht haben). Wenn dann das Met Museum mit Microsoft und Wikimedia kooperiert, um die Kontexte durch ein Bündnis von menschlicher und künstlicher Intelligenz zu erweitern - nämlich Crowdsourcing im Tagging, und algorithmisches Automatisieren der Anwendung der Tags, dann fehlen einfach die radikalen Mathematiker*innen, die diese Technologien mit dem Implex der Museumskritik verbinden können, um ein Topos-Coding durchzuführen, das die Kraft hätte den Raum des Sammelns zu transformieren, so das nichts mehr das Gleiche bliebe. Während die heutigen Code-Künstler*innen großteils im Rausch der KI-Industrie baden, bleiben es einzelne, wie Nora Al-Badri ("any form of (techno)heritage is (data) fiction"), die zum Beispiel in Allianz mit einer marxistischen Kunsthistorikerin die Lektüre des Latent Space gegen das Sammeln wenden (Nora Al-Badri, Wendy M. K. Shaw: Babylonian Vision), und so Institutional Critique digitalisieren.

"Was Künstlerinnen und Künstler seit Erfindung der »Institutional ­Critique«, deren früher erster Blüte auch einige der besten Arbeiten von ­Broodthaers angehörten, an Interventionen in die besagten Räume getragen und dort gezündet haben, von neomarxistischer, feministischer, postkolonialer, medienkritischer, ­queerer Seite und aus unzähligen anderen Affekten und Gedanken, die sich eben nicht allesamt auf eine Adorno’sche »Allergie« wider das Gegebene reduzieren lassen, sondern oft auch aus einer ­Faszination durch dieses, einer Verstrickung in sein Wesen und Wirken geprägt war, liegt in Archiven bereit, die ausgedehnter und zugänglicher sind als je zuvor in der Bildgeschichte. Den Tauschwert dieser Spuren bestimmen allerorten die Lichtmächte. Ihr Gebrauchswert ist weithin unbestimmt. Man sollte anfangen, das zu ändern." Dietmar Dath Sturz durch das Prisma. In: Lichtmächte. Kino – Museum – Galerie – Öffentlichkeit, 2013. S. 45 – 70

[lara635kookie]

Ship Analysis pt.6:

Red Crackle, Carmivy and Carulia.

And about Carmen being mind-wiped he didn't allow to do that. He doesn't have that power. There was nothing he could do to stop Carmen to be brainwashed. We saw how fast V.I.L.E. did it so no one would be able to stop it. Considering the way V.I.L.E. did it, probably everyone that isn't Maelstrom and Doctor Bellum found out that Carmen was evil only after it was already done. And we see is a powerful mind control because Gray heard Doctor Bellum's voice and was exposed to his old V.I.L.E. best friend and didn't remember a thing without the A.C.M.E. machine. So he couldn't just tell evil Carmen about it without V.I.L.E. knowing. And he didn't know how to contact team red so A.C.M.E. really was his only choice.

Another topic is that the only people we see evil Carmen almost killing is Tigress, Zack and Shadowsan. In that order. And Gray clearly wasn't okay with any of these. In the one with Tigress, Gray asks evil Carmen to stop and she stops, simple as that. Look at this, man:

You can't tell me this woman doesn't have a soft spot for Gray. Even in friendship terms, which seems unlikely to me because I have two younger siblings and I don't look to my sister and brother like that. Anyway, the second one is Zack in the ferris wheel. Carmen just warns Gray to stay prepared and act at her signal, but she doesn't explain why and he clearly looks surprised because he didn't know what she was going to do until she does it(that's something that happens a lot with evil Carmen). And the third one is Shadowsan which he could do nothing about because well...He was "dead" on the ground. Coming back to the first one with Tigress, we saw how quickly Carmen listened when Gray told her to stop. Seriously, can you picture dark Carmen listening this fast if it was El Topo, Le Chevre or any other agent? We see Carmen and Crackle were assigned to missions alone, without the rest of their classes. You cannot convince me Crackle was the only one that could calm dark Carmen down. If it wasn't for him, evil Carmen would have killed someone, which doesn't seem to be the case. You cannot tell me V.I.L.E. didn't put them to be assigned partners that always do almost every mission together like El Topo and Le Chevre. Both Carmen and Gray were praised for being one of the best thieves V.I.L.E. ever had. They would only need to kill if they were seen/caught. And together, they wouldn't commit such mistakes. He did say "it was fun while it lasted" but it's another ambiguous, room for multiple interpretations phrases by Gray. I think he meant that having Carmen and his old class with him again, because of the considerations I made of V.I.L.E. before. Honestly, we'll never know for sure what made Gray suddenly decide to help Carmen. Of course he mentions Shadowsan but Gray didn't even care about Shadowsan that much. But he knew Carmen did. And the fact that he decides to help A.C.M.E. because he wants Carmen to be in control of her own path and free his best friend, even willing to go to jail for it, already means he's not truly evil. Yes it took long, but better late than never. Besides, I have a theory that, since Carmen and Gray were assigned partners in crime, and both were the best dynamic power couple duo, V.I.L.E. assigned them to every single possible mission because they knew they wouldn't fail. So my take is that he didn't have the time to act on evil Carmen with Carmen being with him all the time, that's why he does it immediately after Carmen becomes a member of the faculty. Speaking of which, both Carmen and Gray were just back at V.I.L.E. so the faculty had to keep an eye on them. Six months sounds like a fair amount of time to be considered reliable again so after Gray had less faculty eyes on him, he went to A.C.M.E. I feel like, if it wasn't for this factors, he would have done it way before. He was actually smart. It was a clever plan:Waiting for the time to contact A.C.M.E. in the easiest, safest and less likely to go wrong way. So for me it was plenty enough to redeem him. That's what I think.

[yamayuandadu]

It's probably too late for that, but could you do a breakdown of Utu/Shamash?

Not quite sure what do you mean by this, but I can do a quick rundown based on what I wrote on wikipedia long ago if that's what you want. 1. The merge between Utu/Shamash is pretty old, so old that I do not think there's a way to delineate between them. There's a theory that actually the original solar deity of early Akkadian speakers was female, like Shapash in Ugarit or the nameless solar deity in Ebla (the latter is a complex case, I will post about it... eventually) but it's not universally accepted. 2. In addition to the basic solar role, U/Sh. was also responsible for justice and divination. Presumably because going through the sky every day meant he sees everything. His enormous saw attribute might be related to this too, since in both Sumerian and Akkadian, verdicts in legal cases were, to translate the verb literally, "cut". 3. The two primary cult centers of U/Sh. were Sippar and Larsa. Sippar was actually considered older and more venerable, but Larsa had more direct political clout. 4. U/Sh.'s genealogy is virtually invariable, ie. Nanna+Ningal as parents, Inanna as sister (sometimes with bonus siblings like Manzat in Maqlu). His wife is generally consistently the same goddess too, ie. Aya, literally "dawn". Note that Aya's supposed Sumerian name, Sherida, is a possible Akkadian loanword too, from a term referring to red sky in the morning. Their children include figures such as Mamu ("dream", implicitly a meaningful/prophetic one), Kittum ("truth") and so on. Aya has no genealogy and when her relation to any senior deity is ever clarified, it's via her link to her husband, ie. she's only addressed as "daughter in law" (kallatum, literally "bride"). 5. As a Sumerogram, UTU is attested as the writing of virtually every single solar deity from Hattusa to Susa. The Hurrian sun god, Shimige, was pretty closely associated with him in particular, but note the logographic writing did the trick for female solar deities too, like Ugaritic Shapash or Hittite solar goddesses. 6. There are very few, if any, myths focused on U./Sh., but it's effectively a topos that other deities ask him for help: Dumuzi while fleeing the galla, Ninsun in SB Gilgamesh (via Aya), Ninmada in that grain origin myth, etc. Sources are inconsistent about what he was believed to do in the night, and we cannot really neatly chronologically or linguistically delineate whether he was believed to rest or travel through the underworld.

[pv1isalsoimportant]

Broke: sisification

Woke: sheafification

[m---a---x]

Call me the initial object of Cupids topos the way i love noone else

[anomalocariscanadensis]

this article goes into a lot of stuff that's way beyond me, but i think the section on constructive mathematics has a really worthwhile way of looking at things:

Constructive mathematics begins by removing the principle of excluded middle, and therefore the axiom of choice, because choice implies excluded middle. But why would anybody do such an outrageous thing?

I particularly like the analogy with Euclidean geometry. If we remove the parallel postulate, we get absolute geometry, also known as neutral geometry. If after we remove the parallel postulate, we add a suitable axiom, we get hyperbolic geometry, but if we instead add a different suitable axiom we get elliptic geometry. Every theorem of neutral geometry is a theorem of these three geometries, and more geometries. So a neutral proof is more general.

When I say that I am interested in constructive mathematics, most of the time I mean that I am interested in neutral mathematics, so that we simply remove excluded middle and choice, and we don't add anything to replace them. So my constructive definitions and theorems are also definitions and theorems of classical mathematics.

Occasionally, I flirt with axioms that contradict the principle of excluded middle, such as Brouwerian intuitionistic axioms that imply that "all functions (N -> 2) -> N are uniformly continuous", when we equip the set 2 with the discrete topology and N with the product topology, so that we get the Cantor space. The contradiction with classical logic, of course, is that using excluded middle we can define non-continuous functions by cases. Brouwerian intuitionistic mathematics is analogous to hyperbolic or elliptic geometry in this respect. The "constructive" mathematics I am talking about in this post is like neutral geometry, and I would rather call it "neutral mathematics", but then nobody would know what I am talking about. That's not to say that the majority of mathematicians will know what I am talking about if I just say "constructive mathematics".

But it is not (only) the generality of neutral mathematics that I find attractive. Somehow magically, constructions and proofs that don't use excluded middle or choice are automatically programs. The only way to define non-computable things is to use excluded middle or choice. There is no other way. At least not in the underlying type theories of proof assistants such as NuPrl, Coq, Agda and Lean. We don't need to consider Turing machines to establish computability. What is a computable sheaf, anyway? I don't want to pause to consider this question in order to use a sheaf topos to compute a number. We only need to consider sheaves in the usual mathematical sense.

Sometimes people ask me whether I believe in the principle of excluded middle. That would be like asking me whether I believe in the parallel postulate. It is clearly true in Euclidean geometry, clearly false in elliptic and in hyperbolic geometries, and deliberately undecided in neutral geometry. Not only that, in the same way as the parallel postulate defines Euclidean geometry, the principle of excluded middle and the axiom of choice define classical mathematics.

[twocubes]

afaict Johnstone's Sketches of an Elephant is roughly the length of Pact, so ive been like

thinking of stuff i read as two genres: fanfic and wildbow, and the Topos Theory Compendium is in the wildbow genre, while all the papers are in the fanfic genre

[bubbloquacious]

Subobject classifiers of graphs-as-presheaves

Following up on these posts where we view (directed multi-) graphs as set-valued contravariant functors (a.k.a. presheaves) on the small category Q = V ⇉ A, with s,t: V -> A the non-identity morphisms. There's another way in which categories of presheaves such as Q^hat are interesting: they are topoi. An (elementary) topos, following Mac Lane, is a category E that has all finite limits, is cartesian closed, and has a subobject classifier. Supposedly all presheaf categories have this, so let's examine how this manifests itself in graphs.

In particular, I want to check out subobject classifiers. Maybe we'll do limits and cartesian closure at a later date. So in a category C, a subobject of an object A is an isomorphism class of specific kinds of morphisms into A. Let us construct the category Mono(A), whose objects are the monomorphisms into A. A monomorphism (or a morphism that is monic) into A is a C-morphism m: B -> A from some object B such that if f,f': C -> B are parallel morphisms into B such that m ∘ f = m ∘ f', then f = f'. That is, the monos are exactly the left-cancellative morphisms. In the categories of sets, groups, vector spaces, and various other algebraic categories the monos are exactly the morphisms whose underlying set functions are injective, which is why we look at monomorphisms to define subobjects.

The morphisms of Mono(A) from m: B -> A to m': C -> A are the C-morphisms p: B -> C such that m = m' ∘ p. Let's call such morphisms 'factoring morphisms'. If there is a factoring morphism m -> m', we say that m 'factors through' m', denoted m ≤ m'. Clearly the relation ≤ is reflexive and transitive. If both m ≤ m' and m' ≤ m hold, then there are p: B -> C and q: C -> B such that m = m ∘ q ∘ p and m' = m' ∘ p ∘ q. Because m and m' are monic we can cancel them on the left in these equations, from which we find that q ∘ p = id_B and p ∘ q = id_C, so m and m' are isomorphic in Mono(A). Any two isomorphic monos embed their domain into A 'in the same way', so a subobject of A is defined to be an isomorphism class of monos into A. Let Sub(A) denote the set of subobjects of A (technical note: these isomorphism classes may be proper classes, rather than sets; in the case of Q^hat we can pick canonical representatives of the classes, which resolves the issue). The factoring through relation ≤ induces a partial ordering on Sub(A), which coincides with subobject containment in all the familiar cases.

In a category C with a terminal object 1, a subobject classifier is an object Ω of C together with a monomorphism T: 1 -> Ω such that for all objects A,B and monos m: B -> A there is a unique morphism ξ: A -> Ω such that m is a pullback of T along ξ. Rather than unwrap these definitions fully immediately, let's see what this looks like in Set.

If we take Ω = {true,false}, the set of Boolean values, and we let T: {0} -> {true,false} be defined as T(0) = true, then I claim that this forms a subobject classifier for Set (where we assume some background logic of our set theory that includes the principle of excluded middle; otherwise the subobject classifier is more complicated). Let A be a set, and let B ⊆ A be some subset. Let ξ: A -> {true,false} be the function such that ξ(x) = true if x ∈ B and ξ(x) = false if x ∉ B. In Set, a construction of the pullback object of two functions f: Y -> X and g: Z -> X is the set {(y,z) ∈ Y × Z : f(y) = g(z)}. The 'pullback of f along g' is then the projection of this set to Z, and similarly for g along f. What's the pullback of T along ξ? The pullback object is (up to a canonical bijection) the set {(x,0) ∈ A × {0} : ξ(x) = T(0) = true}. There is a canonical bijection between this set and B, and more importantly the inclusion of B into A does the same thing as the projection of the pullback set onto A, because B contains exactly those points x for which ξ(x) = true. It follows that the inclusion function B ↪ A is a pullback of T along ξ.

So, the moral of the story is that Ω is the (object part of the) subobject classifier of some category C if the subobjects Sub(A) of an object correspond naturally to morphisms A -> Ω. We think of ξ: A -> Ω as analogous to the indicator function of a subset, we think of Ω as the set of truth values for 'internal logic' of the category, and we think of T as picking out the subobject of Ω that corresponds to 'true'. I could spin a yarn about why defining this in terms of pullbacks gets you exactly what you want it to be, but this post is long enough already. Tl;dr categorical limits are cool and powerful.

What does Ω look like in Q^hat, our category of graphs? First we would like to know when a graph homomorphism φ: G₁ -> G₂ is monic. A good first guess would be that φ is monic when its vertex and arrow functions φ_V: G₁(V) -> G₂(V), φ_A: G₁(A) -> G₂(A) are injective. This is exactly correct. If we assume that φ_V is not injective, then there are two vertices of G₁ that get mapped onto the same vertex in G₂. It follows that there are two distinct graph homomorphisms from the graph that just has one vertex and no arrows into G₁ such that postcomposing with φ gives you the same homomorphism into G₂ (i.e. φ is not monic). The same holds true if φ_A is not injective, but then there are distinct homomorphisms from the graph that has two vertices and an arrow between them. It is no coincidence, by the way, that these are the graphs よ(V) and よ(A) from my first post on this subject. The representable presheaves always generate the category of presheaves, in the sense that the morphisms out of them together can always 'differentiate' two distinct morphisms. Anyway. If both φ_V and φ_A are injective, then φ is indeed monic, for the same reason that injective functions are monic in Set (it's a nice exercise to work out!).

We've discovered that the subobjects of graphs are exactly the subgraphs. Let's give ourselves a pat on the back for that one. What graph can serve as Ω? Well, the arrow set Ω(A) must contain 5 elements, corresponding to the 5 subgraphs of よ(A). The vertex set Ω(V) has 2 elements, for the 2 subgraphs of よ(V), call them E and P, for 'empty' and 'point'. The source function Ω(s): Ω(A) -> Ω(V) maps a subgraph of よ(A) onto E if it does not contain the source vertex of よ(A) and onto P if it does. The target function Ω(t): Ω(A) -> Ω(V) does the same but for the target vertex instead. Let us write Ω(A) = {a,b,s,t,e}, for 'arrow', 'both points', 'source point', 'target point', and 'empty'. I'm sure you can image which names refer to which subgraph. Both a and b are loops on the vertex P. s is an arrow from P to E. t is an arrow from E to P. e is a loop on E.

The terminal object 1 in Q^hat is the constant functor on a one point set, so as a graph it has a single vertex and a single loop on it. The 'truth' morphism T: 1 -> Ω is the graph homomorphism that picks out the vertex P and the loop a in Ω. On any graph G, we can specify a subgraph G' uniquely by picking out a subset of the vertices and a subset of the arrows of G, such that the source and target of any arrow of G'(A) is also a vertex of G'(V). We construct the indicator homomorphism ξ: G -> Ω as mapping all vertices of G' onto P and all vertices not in G' onto E. Furthermore, an arrow gets mapped onto a if and only if it is an arrow of G'. This is actually enough to uniquely specify ξ, but let's work it out some more. Arrows that connect vertices that are not in G' get mapped onto e. Arrows from a vertex of G' to one outside it get mapped to s. The other way round get mapped to t. Arrows between vertices of G' that are not arrows of G' get mapped to b. And there you go! The subobject classifier for the category of graphs :)

[branded-perceptions]

Irony is a mimetic dialectic means that can bridge, t-ease and mimetically incentivise to question and look behind the subjective reductionistic nerd "seriousness" (like autistic $cience : 🔍list of psychological biases)

of any for median life causally disfunctional self-justifications & ideologies & rationalisations

[whose AUTHORITY depends on its AUTHENTICITY which is challenged via sensing significance of spectrum of (double, triple, quadripple layered) IRONY you see?]

of all the many "opposing" subjective psychosis' in-group mythos

(white bear problem: consciousness and every subjective argumentation is a type of psychosis by definition on a scale of introspective self-awareness: meta-cognition)

bubbles🎈 self-justification loops

(metaphorical "ARITY master functions" of ai-tech = familiARITY entrainment / entertainment)

via what to the ironically "serious" in-group mass psychosis due projection subjectively appears as schizophrenia (projection of their own ailment which they are "confidently" unaware of / via status constructs and peer-reinforcement convinced to not be posessed by due rarely questioning their own familiARITY constructs of their minds)

depending on their stage of systems thinking awareness (reality testing: the judgment)

on scale of subjectivitsm and objectivity as explored by 🔍9 stages of increasing ego-development by Susanne R Cook-Greuter:

what to some appears as satire / ironic / comedy appears serious to others and vice-versa on a nuanced scale of significance depending on their logic systems thinking comprehension of complex nuances' objective reality interplaying with the nerd and by status charged "Quantum world"

[Black cube idiocracy: many overcomplexified and with status charged "scientific" theories are nothing but a from causalities' relation to our life force detached ironic joke but your (mathematical) understanding of this (📚Higher topos theory Jacob Lurie) depends on your own self-reflective abilities: WHO ARE YOU? Analyse etymology of human / humus earth and ponder about its meanings ... Do you pay more attention to bra(i)nde(a)d stories and $studies or actual causal effects of the "hummus" you eat? Ponder about that and you shall become conscious about "Quantum world" which is a metaphor for scale of meta-cognitive irony between social interfaces of many "different" subjective fictions and objective reality: The word quantum is the neuter singular of the Latin interrogative adjective quantus, meaning "how much"? ("How much" close to objective realities elementary relation to our life force are you mentally?) Quantum world can be seen as an ironic metaphor for fluid scale of differentiation between sanity and insanity]

of our "different" subjective models and fil(l/t)ers of it: 🔍list of cognitive biases.

Similar like medieval nursery rhymes IRONIC

entertainment

can counterbalance the for mean median life force disfunctional social FANTASIES' status "heaven"🤥😷😇 psychotic unconsciously emotionally charged (🔍Plato cage) in-group identity

entrainment

(covert fascism) of PUBLIC and PRIVATE sector

without that those lost in mass psychosis realise as they mistakenly believe it would all be just jokes and they would be the ones that would be "serious" which then might change when psychological reality testing (the judgement) kicks in which depends on ability of systems thinking as some causal aspects accumulate in a larger systems picture while their (similar as C-19 vaccine side-effects overlap with long-covid) with other supposedly "objective" but already biased and pre-filtered data feedback mingling staying unseen to the "reality testing" of those lost in more polarising reductionistic understanding as seen as just one example via 🔍Dr. Shiva ayyadurai explains modern theory of immune system.

You can highlight the due psychosis

(white bear problem which becomes only obvious to those who are not caught up in it ... the joy of searching for self-irony helps you to stay more sane statistically and is antidote to a number of mental health issues. Do you (not consciously know that you potentially) have any psychological problems? Try to be more ironic about it out of own motivation to via such nonsense sooner or later focus on and authenticity and it will be gone: have you ever seen a depressed person overcoming its mood via being teased by friends with irony about depression mirroring as if they themselves would be depressed while incentivising causal habits that help biology of that person grow out of it? Works better than most pharmaceutical drugs, but it cannot be as much commercialised thus it is widely ignored by medical sector! Similarly, if you read my content here about the irony of our collective socio-psychological dynamics it will help you overcome it via by it incentivised causal problem solving: preferably via joy of embracing goofy self-irony (grace) about past insanity instead of "serious" continued psychotic denial whose continuation, if you have social responsibilities, indeed might be a case for psychiatry)

of how you can highlight the due psychosis neglected difference of policy-making and its from actual realities' data feedback divergent perceptions of past events via irony in order to drive attention to thereby more on validy gaining anti-theses deivibg synthesis: irony is a mimetic form of dialectics t-easing "opposing" reductionistic nerd views' in-group psychosis. But there is a danger:

Medieval nursery rhymes where indirectly killing / in dangerous aggressive ways entertainingly humiliating those public personas / medieval celebrities that violated the causal basic life boundaries of common people that thus as "mad mob"

via their by that in more cohersive ways formed untempered impulsivity

[[scapegoating creates in-group coesion as people then can A) blame parts of their struggles upon an external scapegoat B) understand their normalised ungraspable complex impersonal in-group insanity through a personal graspable blamed scapegoat story whose behavioral and philosophical lessons helps the group to peer-pressure itself in eays to evolve out of its own mass insanity of previously in this regard miscslibrated peer-pressure without needing to blame itself / without needing people to use their brain for self-reflection / without needing the IQ-devoid masses with their harsh daily life (where most had no time to ponder and introspect so much) to understand the here explained complex nuanced systems dynamics]]

protected their swarm by altering these stories that strove to direct the frustrations and aggressions of people towards via scapegoat stories' behavioral lessons helping them evolve out of the struggles that triggered it via by their abusers as "positive" storytelled common life boundary violations💸💉☠️💉💸 .

Nowadays the back then functional cruelty of this is outdated because now via new media technologies we have the means to instead of reductionistically scapegoating anyone being able to discuss and make more widely the complex nuanced systems dynamics of it and how as example in current geopolitical conflicts or mishandling of C-19 pandemic we all played our parts in some ways, not just some isolated figures.

Nevertheless we need graspable personalities and stories to understand the complex impersonal social systems dynamics which otherwise most in their subjective bubble do not take serious and cannot comprehend.

As currently our group-insanities symbolic projections concentrate in our worldwide religion of bra(i)nde(a)d perceptions of consumer go(o)d(s)

and Gary Vee, one of the most famous "expert" in exactly that, has voiced that his biggest dream would be (quote) that everyone shits on him & he gets burned to the ground

thus he seems most suitable and morally justifiable story scapegoat to understand our group-insanities which his online content embodies as social focal lense:

but the importance is the differentiation of fiction and reality.

It can be morally just and desirable to make fun about the mythos insanity of any suitable scapegoat (including myself) via satire and dead serious jokes to via authenticity (or preferably goofy self-irony: grace) drive attention towards causal problem solving of issues that matter to us all

but simultaneously it is immoral and injust to try to bring physical harm or over-blame people like Gary who are just an exaggerated personified bra(i)nde(a)d story focal lense and themselves are non-violent, subjectively trying to do their best according to their limited understanding or impaired mind. If a kid misbehaves, you do not beat it, you calmly introspect with it about its misbehaviours similar like I do here on my account lile a healthy father figure should do which in society would be the job of the state:

imagine if our policians instead of bullying each other like Kindergarten would publicly introspect (intimacy) with us all about all our collective misbehaviours (and via goofy irony about their own) so we can problem-solve the systematic root causes via shared trial and error which will continue to need endless introspection and self-reflection as also shown a bit in movie "Star Trek":

the Vulcanians are storytelled symbol for rationalism which rescued humanity from its irrational group-insanities, but also simultaneously at one Episode humanity rescued the Vulcanians with our human key trait:

(Goofy) ironies intersection with group motivations' mimetic effects' identity management🎭.

Irony helps to become more conscious of and look behind the white bear problem of peer-pressures' mass psychosis of in-group identity mythos: what to some appears ironic appears serious to others and vice-versa depending on your stage of rational comprehension of nuances of objective realities' interplay with in-groups' subjective relativism.